$\forall$$p$:(:$\mathbb{N}$ $\times$ $\mathbb{N}$). inc{-}snd($p$) $\in$ (:$\mathbb{N}$ $\times$ $\mathbb{N}$)